FDL - Nuprl Lemma : weak-antecedent-surjection-conditional2

Nuprl Lemma : weak-antecedent-surjection-conditional2

es:ES, P1, Q1, P2, Q2:(E

), dcd_P1:(e:E

Dec(P1(e))), f:({e:E| P1(e)}

{e:E| Q1(e)} ),

g:({e:E| P2(e)}

{e:E| Q2(e)} ).
(

e:E. (P1(e))

(

(P2(e))))

(

e:E. Dec(Q1(e)))

(

e:E. Dec(Q2(e)))

Q1

= f== P1

Q2

= g== P2

Q1

Q2

= [P1? f : g]== P1

P2

Definitions P1 P2

Lemmas weak-antecedent-surjection-conditional